Nuprl Lemma : p-fun-exp-one
11,40
postcript
pdf
A
:Type,
f
:(
A
(
A
+ Top)).
f
^1 =
f
latex
ProofTree
Definitions
f
^
n
,
Type
,
s
=
t
,
x
:
A
B
(
x
)
,
left
+
right
,
Top
,
x
:
A
.
B
(
x
)
,
t
T
Lemmas
p-compose-id
origin
A:Type, f:(A
(A + Top)). f^1 = f
A:Type, f:(A(A + Top)). f^1 = f
B(x)x:A. B(x)
T